% Chapter 1

\chapter{Implementare}
\label{Capitolul6}

Pentru a exemplifica modul \^ in care sistemul de tipuri poate fi folosit pentru a verifica terminarea programelor, am implementat un compilator pentru un limbaj de programare func\c tional\u a - \textbf{TBT} - bazat pe System \fhat. Urmatoarea diagram\u a este o vedere de ansamblu asupra diverselor sisteme de tipuri prezentate p\^ an\u a acum \c si a propriet\u a\c tilor lor.

\done\todo{big picture}
\begin{center}
\input{Imagini/overview.tex}
\end{center}

\section{Compilatorul}
% 1 pag
Una din marile diferen\c te \^ intre System \fhat \c si un limbaj de programare func\c tional\u a este sintaxa potrivit\u a mai degraba pentru demonstra\c tii dec\^ at pentru scrierea de programe. Acest lucru se poate rezolva de c\u atre compilator prin diverse manipul\u ari sintactice (syntactic sugar).

\begin{example}
Am folosit declara\c tii globale asem\u an\u atoare celor din Haskell :\\
\texttt{\scriptsize let <X1> f1 := e1 ;} \\
\texttt{\scriptsize let <X2> f2 := e2 ;} \\
\texttt{\scriptsize body}\\
care se translateaz\u a \^ in System \fhat in $(\lambda f_1 : X_1. (\lambda f_2 : X_2. body)\app e_2) \app e_1$. Declara\c tiile de func\c tii sunt exprimate ca \texttt{\scriptsize fn <X> arg => body} \c si se translateaz\u a \^ in $\lambda arg : X.body$.
\end{example}

Un exemplu complet de program TBT este \^ in este cel de mai jos.
\begin{lstlisting}[label=impl_example,captionpos=b,caption=Exemplu de program complet]
-- Liste polimorfice
Inductive List X = nil  : List X
                   cons : X -> List X -> List X ;
-- Numere naturale
Inductive Nat    = z : Nat
                   s : Nat -> Nat  ;
-- Functie de adunare a doua numere naturale
let |<Nat->Nat->Nat>| add :=
        (letrec|<Nat->Nat->Nat>| add_ :=
            fn|<Nat>| x => fn|<Nat>| y =>
                case|<Nat>| x of {
                    z => y
                    s => fn|<Nat>| px => ((add_ px) (s y))
                }
       );
-- Programul principal
(cons |<Nat>|
    (add z (s z))
    (cons |<Nat>|
        (z)
        (nil |<Nat>|)))
\end{lstlisting}

Compilatorul transform\u a programe de genul celui de mai sus \^ in cod Java folosind mecanismul de \^ inchideri func\c tionale \citep{DBLP:books/wi/GruneBJL2002}. Fiecare func\c tie Sytem \fhat este compilat\u a intr-o clas\u a Java ce extinde clasa \texttt{Closure} ce con\c tine o referint\u a c\u atre \^ inchiderea p\u arinte \c si o mapare \^ intre numele argumentului \c si valoarea acestuia (ini\c tial maparea este vid\u a, pan\u a c\^ and func\c tia este aplicat\u a). La aplicarea unei func\c tii, se stabile\c ste leg\u atura \^ intre numele parametrului \c si \^ inchiderea care este reprezentat\u a de acesta. O variabil\u a se caut\u a pe lan\c tul de parin\c ti de inchideri func\c tionale p\^ an\u a c\^ and se gase\c ste o asociere valid\u a pentru numele ei. Un exemplu de \^ inchidere sunt constructorii care pur \c si simplu acumuleaz\u a parametri asupra c\u arora sunt aplica\c ti. \^ In cazul unei expresii \emph{case}, se stabile\c ste tipul construtorului \c si argumentele acumulate de acesta sunt furnizate func\c tiei de pe ramura corespunz\u atoare.

Strategia de evaluare folosit\u a este una \emph{call-by-value} mo\c stenit\u a din Java. Datorit\u a proprieta\c tii System \frec, \c si deci System \fhat, de normalizare puternic\u a \c si de conluen\c ta (folosind rela\c tia de reducere $\to_{\beta\iota\mu}$), termenii au o form\u a normal\u a unic\u a. Formele normale pentru aceast\u a strategie sunt incluse \^ in mul\c timea de forme normale pentru strategia lene\c s\u a. Pentru a afi\c a rezultatul programului acesta trebuie adus \^ in \emph{head normal form}, adic\u a aplica\c tiile de contructori nu mai sunt forme normale. 

Pentru parsare \c si generare de cod am folosit ANTLR \c si StringTemplate, codul fiind scris \^ in Java.

\section{Algoritmul de verificare a tipurilor}
% 1 pag

Regulile de tip prezentate \^ in sec\c tiunea \ref{reguli_sysfhat} au dezavantajul ca \^ in aplicarea lor trebuie s\u a se \emph{ghiceasca} adnot\u arile cu dimensiuni pentru unele tipuri. Solu\c tia acestei probleme \citep{DBLP:conf/tlca/BartheGP05} este a\-se\-m\u a\-n\u a\-to\-a\-re cu cea folosit\u a \^ in sistemului de tipuri Hindley-Milner \citep{ATTAPL}, \c si anume, de fiecare dat\u a c\^ and adnot\u arile trebuiesc \emph{ghicite}, acestea se \^ inlocuiesc cu \emph{variablie de deduc\c tie} cuantificate universal peste toat\u a expresia de tip (func\c tiile annot \c si annotrec din \fref{ver_alg}). Apoi, pe masur\u a ce regulile de tip sunt aplicate, se acumuleaz\u a constr\^ angeri asupra acestor variabile. Tipul unei expresii are forma $C \Rightarrow \overline{\tau}$ cu $\overline{\tau}$ un tip adnotat cu variabile de dimensiune \c si $C$ o multime de constr\^ angeri \^ intre aceste dimensiuni. Noile reguli de tip sunt prezentate \^ in pseudocod \^ in \fref{ver_alg}.


\subsection{Noile reguli de tip}

Pentru claritate, algoritmul este implementat de dou\u a func\c tii mutual recursive: \textbf{Infer} \c si \textbf{Check}. Func\c tia \textbf{Infer} deduce tipul adnotat al unei expresii, \^ in timp ce \textbf{Check} verific\u a dac\u a o expresie are un anumit tip. Ca \c si variabile globale se folosesc: o mul\c time de constr\^ angeri care se acumuleaz\u a pe masura verific\u arilor, contextul de tip \^ in care se desfasoar\u a algloritmul \c si mul\c timea de variabile care au fost deja folosite.

Constr\^ angerile sunt reprezentate de inegalit\u a\c ti \^ intre dimensiuni, constr\^ angerea \emph{false}, sau constr\^ angeri rezultate din rela\c tia de subtip. O solu\c tie pentru o mul\c time de constr\^ angeri este o substitu\c tie a variabilelor de dimensiune cu expresii de dimensiune, pentru care toate inegalit\u a\c tile pot fi demonstrate conform regulilor care dau rela\c tia de ordine \^ intre dimensiuni. De remarcat c\u a dac\u a \^ in setul de constr\^ angeri nu exist\u a \emph{false}, atunci prin \^ inlocuirea tuturor variabilelor cu $\infty$, se ob\c tine o solu\c tie. Deci dac\u a \^ in setul de constr\^ angeri nu apare constr\^ angerea \emph{false}, atunci exista cel pu\c tin un tip care se poate deduce pentru expresia verificat\u a.

\done\todo{algoritm + annot +annotrec + Check + Infer}
\begin{figure}
\begin{align*}
\textbf{Check} (V,\overline{\Gamma},e,\overline{\tau}) =
    &(V_e, C_e \cup \overline{\tau}_e \sqsubseteq \overline{\tau}) \text{ unde } \\
    &(V_e, C_e, \overline{\tau}_e) := \textbf{Infer}(\overline{\Gamma},e)\\
\textbf{Infer}(V,\overline{\Gamma},x) =
    &(V,\emptyset,\overline{\Gamma}(x))\\
\textbf{Infer} (V,\overline{\Gamma}, \lambda x : \tau.e) =
    &(V_e, C_e, \overline{\tau}_1 \to \overline{\tau}_2) \text{ unde } \\
    &(V_1,\overline{\tau}) := \textbf {annot} ( V, \overline{\tau}_1) \\
    &(V_e,C_e,\overline{\tau}_2):= \textbf{Infer}(V_1, \overline{\Gamma};x: \overline{\tau}_1,e)\\
\textbf{Infer} (V,\overline{\Gamma}, \Lambda X.e) =
    & (V_e, C_e,\Pi X.\overline{\tau}) \text{ unde }\\
    & (V_e, C_e, \overline{\tau}_e) := \textbf{Infer}(V,\overline{\Gamma},e)  \text{ daca X nu apare in } \overline{\Gamma} \\
\textbf{Infer}(V,\overline{\Gamma},e_1\app e_2)   =
    & (V_2, C_1 \cup C_2, \overline{\tau}_2) \text { unde } \\
    & (V_1, C_1, \overline{\tau}_1 \to \overline{\tau}_2) := \textbf{Infer}(V,\overline{\Gamma},e_1) \\
    & (V_2, C_2) :=  \textbf{Check}(V_1,\overline{\Gamma},e_2, \tau_1) \\
\textbf{Infer}(V,\overline{\Gamma},e_1\app [\tau])   =
    & (V_e, C_e, [X \mapsto \overline{\tau}]\overline{\tau}_e) \text { unde }\\
    & (V_1,\overline{\tau}) := \textbf{annot}(V,\tau) \\
    & (V_e, C_e, \Pi X.  \overline{\tau}_e)) := \textbf{Infer}(V_1,\overline{\Gamma},e) \\
\textbf{Infer}(V,\overline{\Gamma},c)   =
    &(V \cup \{\alpha\}, [\iota \mapsto \alpha] (\Pi X. \theta \to d^{\hat{\iota}}\app X)) \text{ unde } \alpha \notin V \\
\textbf{Infer}(V,\overline{\Gamma}, \text{case}_\sigma\ e \text{ of } \{ c_i \Rightarrow e_i\}) =
    & (V_n, s \le \hat{\alpha} \cup \bigcup C_i, \overline{\sigma} \text{ unde } \alpha \notin V \\
    & (V_{\sigma}, \overline{\sigma}) := \textbf{annot}(V\cup \{\alpha\}, \sigma) \\
    & (V_0, C_e, d^s\app \overline{\tau}) := \textbf{Infer}(V_\sigma,\overline{\Gamma},e) \\
    & (V_i, C_i) := \textbf{Check}(V_{i-1},\overline{\Gamma}, e_i, [\iota \mapsto \alpha, X\mapsto \overline{\tau}] \theta \to \sigma)\\
\textbf{Infer}(V,\overline{\Gamma}, \text{letrec}_{d^{\star}\tau\to \sigma} f := g) =
    &(V_g,C_r,d^{\alpha}\app\overline{\tau}\to\overline{\sigma})  \text{ unde } \\
    &(V_1, V^\star, d^\alpha\app\overline{\tau}\to\overline{\sigma}) := \textbf{annotrec}(V,d^\star\tau\to\sigma) \\
    &\widehat{\sigma} := [(\iota \mapsto \hat{\iota})_{\iota\in V^\star}]\overline{\sigma}\\
    &(V_g, C_g) := \textbf{Check}(V_1,(\overline{\Gamma},f:d^{\alpha}\app\overline{\tau}\to\overline{\sigma}),g,d^{\hat{\alpha}}
    \app \overline{\tau} \to \widehat{\sigma} )\\
    & C_r := \textbf{RecCheck}(\alpha, V^\star,V^\neq=V_1\setminus V^\star,C_g \cup \overline{\sigma} \sqsubseteq \widehat{\sigma})
\end{align*}
\caption{Algoritmul de verificare a tipului}
\label{ver_alg}
\end{figure}

\subsection{Verificarea pentru letrec}
% enunt cei 8 pasi
\done\todo{pasii si de ce trebuie separate var din letrec}
Pentru a putea fi aplicate, regulile {\scriptsize (T-ABS), (T-TAPP)} \c si {\scriptsize (T-CASE)} au nevoie de existen\c ta unor adnot\u ari cu dimensiuni ale tipurilor specificate \^ in sintaxa lor care s\u a satisfac\u a ipotezele. Acest lucru se traduce prin existen\c ta unei substitu\c tii pentru variabilele de deduc\c tie introduse de algortimul din \fref{ver_alg}, care s\u a satisfac\u a mul\c timea de constr\^ angeri acumulat\u a.

Pentru regula {\scriptsize (T-LETREC)} \^ insa, condi\c tia este s\u a existe o substitu\c tie $\rho$ astfel \^ inc\^ at $[\iota \mapsto s]\rho$ s\u a satisfac\u a $C$ pentru orice $s$ a c\u arei valoare nu este de forma $\hat{\jmath}^k$ cu $\jmath \in \overline{\Gamma}, \overline{\tau}$. Pentru a codifica aceast\u a condi\c tie \emph{universal\u a} prin una \emph{existential\u a}, \textbf{RecCheck} trebuie s\u a modifice mul\c timea de constr\^ angeri $C$ astfel \^ incat s\u a elimine toate constr\^ angerile ce implic\u a variabila $\alpha$ folosit\u a pentru adnotarea argumentului func\c tiei textual recursive \c si a celorlalte pozi\c tii marcate cu $\star$. Acest lucru se face prin substituirea tuturor celorlalte variabile implicate \c in astfel de constr\^ angeri cu $\infty$. Atunci cand acest lucru implica $\infty \le \alpha$, se adauga constr\^ angerea \emph{false} semanl\^ and c\u a nu poate fi stabilit un tip pentru expresia dorit\u a.

\done\todo{pe scurt trebuie ca orice substitutie sa nu combine variabilele}
\emph{Variabila de baz\u a} a unei dimensiuni $\hat{\iota}^k$ este $\iota$. Pa\c sii urma\c ti de algoritm sunt prezenta\c ti \^ in continuare:
\begin{enumerate*}
\item $S_\iota$ := mul\c timea de variabile care trebuie substituite cu dimensiuni care au variabila de baz\u a aceeasi cu a lui $\alpha$. Regula de formare este $V^\star \subseteq S_\iota,\forall \alpha_1 \in S_\iota, \hat{\alpha}^{n_2}_2 \sqsubseteq \hat{\alpha}^{n_1}_1 \Rightarrow \alpha_2 \in S_\iota $.
\item $\alpha$ trebuie sa fie cea mai mic\u a dintre dimensiunile cu aceea\c si variabil\u a de baz\u a. Adic\u a $C_1 := C \cup \bigcup_{s\in S_i}\alpha \sqsubseteq s$.
\item Dac\u a \^ intre variabile exist\u a cicluri negative de genul $\hat{\imath} \le \jmath, \jmath \le \imath $, singura variant\u a de a satisface constr\^ angerile este de a substitui toate variabilele implicate \^ in astfel de cicluri prin $\infty$, adic\u a  putem \^ inlocui toate constr\^ angerile ce formeaz\u a un ciclu negativ cu o multime de constr\^ angeri $\infty \le \imath$ obtin\^andu-se astfel $C_2$.
\item $S_{\iota\le}$ := mul\c timea de variabile care trebuie substituite prin $\infty$ sau o dimensiune cu variabil\u a de baz\u a aceea\c si cu a lui $\alpha$. Adic\u a, $S_\iota \subseteq S_{\iota\le}$ \c si $\forall \alpha_1 \in S_{\iota\le}.\: \hat{\alpha}^{n_1}_1 \sqsubseteq \hat{\alpha}^{n_2}_2 \Rightarrow \alpha_2 \in S_{\iota\le}$.
\item $S_{\neg \iota}$ := mul\c timea de variabile care trebuie substituite prin dimensiuni cu variabil\u a de baz\u a diferit\u a de cea a lui $\alpha$. Adic\u a, $V^\neq \subseteq S_{\neg \iota}$ \c si $\forall \alpha_1 \in S_{\neg \iota}.\: \hat{\alpha}^{n_1}_1 \sqsubseteq \hat{\alpha}^{n_2}_2 \Rightarrow \alpha_2 \in S_{\neg\le}$.
\item $C_3 := C_2 \cup \bigcup_{s \in S_{\neg \iota} \cap S_{\iota\le}} \infty \le s$.
\item $S_\infty$ := mul\c timea variabilelor care trebuiesc substituite cu $\infty$. Adic\u a dac\u a $\infty\le s \in C_3 \Rightarrow s \in S_\infty$ \c si $\forall \alpha_1 \in S_\infty.\: \hat{\alpha}^{n_1}_1 \sqsubseteq \hat{\alpha}^{n_2}_2 \Rightarrow \alpha_2 \in S_\infty$.
\item Dac\u a exist\u a variabile care au variabila de baz\u a $\iota$ (egal\u a cu cea a lui $\alpha$), \c si care trebuie substituite prin $\infty$, atunci \^ inseamna c\u a ipoteza regulii {\scriptsize (T-LETREC)} nu este adevarat\u a pentru $\forall \iota$ ci doar pentru o alegere particular\u a. Atunci setul de constr\^ angeri returnat este $\{false\}$, altfel este $C_3$.
\end{enumerate*}
\done\todo{continuat pasii}
\subsection{Corectitudinea algoritmului}
% algoritmul este corect => exista solutie la constrangeir daca si numai daca se termina
Faptul ca algoritmul de verificare prezentat func\c tioneaza conform regulilor din sec\c tiunea \ref{reguli_sysfhat}, este garantat de urm\u atoarea teorem\u a \citep{DBLP:conf/tlca/BartheGP05}
\done\todo{daca ex o sub a var care sa sat C, at ex o subst si pentru reg initiale}
\begin{theorem}
$\textbf{\emph{Infer}}(\emptyset,\emptyset,e) = (\_,C,\overline{\tau})$ \c si exist\u a o substitu\c tie $\rho$ a variabilelor de dimensiune prin dimensiuni care s\u a satisfac\u a pe $C$, dac\u a \c si numai dac\u a se poate deduce c\u a $\emptyset \vdash e : \rho(\overline{\tau})$ conform regulilor din sec\c tiunea \ref{reguli_sysfhat}.
\end{theorem}

\begin{comment}
\section{Demonstratia in \LaTeX{}}
% 0.5 pag
Compilatorul poate genera un fisier \LaTeX{} care sa contina demonstratia terminarii programului conform regulilor de tip.
\todo{concret cum fac?}
\end{comment} 